$\forall$$T$:Type, $l$:($T$ List). ($\parallel$$l$$\parallel$ = 0) $\Leftarrow\!\Rightarrow$ ($l$ = [])